$\forall$$T$:Type, $l_{1}$:($T$ List), $v$:$T$, $l_{2}$:($T$ List).
\\[0ex]fseg($T$;$l_{1}$;$l_{2}$)
\\[0ex]$\Rightarrow$ (($\parallel$$l_{1}$$\parallel$ $<$ $\parallel$$l_{2}$$\parallel$) c$\wedge$ ($l_{2}$[($\parallel$$l_{2}$$\parallel$ {-} ($\parallel$$l_{1}$$\parallel$+1))] = $v$))
\\[0ex]$\Rightarrow$ fseg($T$;[$v$ / $l_{1}$];$l_{2}$)